R-occurs(R;i;z)
== case R of 
== Rnone => false
== Rplus(left,right)=>rec1,rec2.rec1  rec2
== Rinit(loc,T,x,v)=> loc = i  z = x
== Rframe(loc,T,x,L)=> loc = i  z = x
== Rsframe(lnk,tag,L)=> false
== Reffect(loc,ds,knd,T,x,f)=> loc = i  (z = x  z  dom(ds))
== Rsends(ds,knd,T,l,dt,g)=> source(l) = i  z  dom(ds)
== Rpre(loc,ds,a,T,P)=> loc = i  z  dom(ds)
== Raframe(loc,k,L)=> loc = i  deq-member(IdDeq;z;L)
== Rbframe(loc,k,L)=> false
== Rrframe(loc,x,L)=> loc = i  z = x 

latex

---

clarification:

R-occurs(R;i;z)
== case R of 
== Rnone => false
== Rplus(left,right)=>rec1,rec2.rec1  rec2
== Rinit(loc,T,x,v)=> loc = i  z = x
== Rframe(loc,T,x,L)=> loc = i  z = x
== Rsframe(lnk,tag,L)=> false
== Reffect(loc,ds,knd,T,x,f)=> loc = i  (z = x  fpf-dom(IdDeq; z; ds))
== Rsends(ds,knd,T,l,dt,g)=> source(l) = i  fpf-dom(IdDeq; z; ds)
== Rpre(loc,ds,a,T,P)=> loc = i  fpf-dom(IdDeq; z; ds)
== Raframe(loc,k,L)=> loc = i  deq-member(IdDeq;z;L)
== Rbframe(loc,k,L)=> false
== Rrframe(loc,x,L)=> loc = i  z = x 

latex

Definitions	es realizer ind, p  q, source(l), x  dom(f), deq-member(eq;x;L), IdDeq, false, p  q, a = b
FDL editor aliases	R-occurs